/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.Iterator;
import java.util.Set;

import alloy.ast.Expr;
import alloy.ast.Leaf;
import alloy.transl.ASTInfo;
import alloy.transl.ExprTransl;
import alloy.transl.RelationAllocator;
import alloy.transl.TranslInfo;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.util.Dbg;

/**
 * Special symmetry-breaking for binary homogeneous relations constrained
 * to be DAGs (directed acyclic graphs).  We can require that the adjacency
 * matrix of the DAG (i.e. the relation) be upper triangular: any instance
 * can be transformed into an isomorphic instance in which the relation is
 * upper triangular, by topologically sorting the DAG and exchanging the
 * vertices accordingly.  That's when all atoms are interchangeable.
 * More generally, if there is a group of interchangeable atoms then
 * the submatrix for such a group can be made lower-triangular.
 */
class SBM_DAG extends SymmetryBreakingMethod {

    /** AST nodes representing homogeneous binary relations constrained to be DAGs */
    private Set /* of Expr */ _dags;

    /**
     * Whether we should only use DAGs that are leaves (relations) -- this can be done
     * before translation; or should also use DAGs that are internal AST nodes --
     * but this can only be done after translation (and requires {@link #_astInfo}
     * to be an instance of {@link TranslInfo} and provide translations of all nodes).
     */
    private boolean _onlyLeafDAGs;

    //////////////
    // Methods //
    ////////////

    SBM_DAG(ASTInfo astInfo_, RelationAllocator relAlloc_, boolean onlyLeafDAGs_) {
        super(astInfo_, relAlloc_);
        _onlyLeafDAGs = onlyLeafDAGs_;
        Dbg.chk(_onlyLeafDAGs || (astInfo_ instanceof TranslInfo));
        // detect homogeneous binary relations constrained to be DAGs.
        // this will detect general expressions constrained to be DAGs --
        // not necessarily leaves.
        DAGDetector_V dagDetector = new DAGDetector_V(astInfo_);
        astInfo_.getFormula().applyVisitor(dagDetector);
        _dags = dagDetector.getDAGs();
    }

    /**
     * Break DAG symmetry by requiring the adjacency matrix of a DAG to be upper triangular.
     */
    SymmetryBreakingPredicate breakSymmetry(AvailableSymmetry availSymm_,
                                            Set/*<BasicType>*/ basicTypes_) {
        SymmetryBreakingPredicate sbp = new SymmetryBreakingPredicate();
        for (Iterator dagIter = _dags.iterator(); dagIter.hasNext();) {
            Expr dag = (Expr)dagIter.next();
            if (_onlyLeafDAGs && !(dag instanceof Leaf))
            continue;
            ExprTransl dagTransl =
            _onlyLeafDAGs ? _relAlloc.getRelationTransl(((Leaf)dag).getLeafId()) :
            (ExprTransl)((TranslInfo)_astInfo).getNodeTransl(dag);
            RelationType relType = dag.getType().toRelationType();
            Dbg.chk(relType.numBasicTypes()==2 && relType.getBasicTypeAt(0).equals(relType.getBasicTypeAt(1)));
            BasicType btype = relType.getBasicTypeAt(0);
            Set/*<AtomSet>*/ symmSets = (Set)availSymm_.getSymmSets(btype);
            for (Iterator symmSetIter = symmSets.iterator(); symmSetIter.hasNext();) {
            AtomSet symmSet = (AtomSet)symmSetIter.next();
            // System.out.println("Breaking DAG symm: " + dag.nodeString() +
            //                    " " + dag.getType() + " " + symmSet);

            int symmSetSize = symmSet.size();
            for (int i=0; i<symmSetSize; i++)
                for (int j=i; j<symmSetSize; j++)
                sbp.conjoin(dagTransl.getTupleFormula(symmSet.getAtomAt(i),
                                      symmSet.getAtomAt(j)).not());
            }  // loop over symmsets of basic type btype
            availSymm_.removeAllSymmetry(btype);
        }  // loop over Exprs constrained to be DAGs

        return sbp;
    }  // breakSymmetry()

}  // class SBM_DAG
